Termination w.r.t. Q proof of TRS/higher-order/AotoYam006.trs

Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

app(app(mapbt, f), app(leaf, x)) → app(leaf, app(f, x))
app(app(mapbt, f), app(app(app(branch, x), l), r)) → app(app(app(branch, app(f, x)), app(app(mapbt, f), l)), app(app(mapbt, f), r))

Q is empty.

↳ QTRS

Q restricted rewrite system:
The TRS R consists of the following rules:

app(app(mapbt, f), app(leaf, x)) → app(leaf, app(f, x))
app(app(mapbt, f), app(app(app(branch, x), l), r)) → app(app(app(branch, app(f, x)), app(app(mapbt, f), l)), app(app(mapbt, f), r))

Q is empty.